T:Type, l:(T List), x:T. (x  l)  (l1,l2:T List. (l = (l1 @ [x] @ l2))) 

latex

Definitions	x:A. B(x), (x  l), P  Q, x:A. B(x), P  Q, P  Q, P & Q, P  Q, t  T, , as @ bs, False, x. t(x), Dec(P), ||as||, i  j , hd(l), A, A  B, tl(l), {T}
Lemmas	member append, or functionality wrt iff, ge wf, tl wf, hd wf, non neg length, length wf1, append is nil, decidable false, cons member, all functionality wrt iff, iff functionality wrt iff, nil member, false wf, append wf, iff wf, l member wf